w:World. FairFifo  (e:E. no_repeats(E;eventlist(e.w-pred(w;e);e))) 

latex

Definitions	World, t  T, x:A. B(x), FairFifo, no_repeats(T;l), P  Q, w-pred(w;e), x.A(x), pred(e), E, s = t, first(e), b, A, A & B, SWellFounded(R(x;y)), w-info(w;e), Id, sender(e), rcv?(e), Type, Prop, x:AB(x), P  Q, pred!(e;e'), x:AB(x), a<b, , {x:A| B(x) }, f(a), x:A. B(x), P & Q, EOrderAxioms(E; pred?; info), Void, False, x f y, P  Q, eventlist(pred?;e), x before y  l, P  Q, time(e)
Lemmas	w-cless-loc, w locl-lemma, w-time wf, no repeats iff, l before wf, eventlist wf, l before eventlist iff, w-order-axioms, nat wf, not wf, first wf, pred wf, w-pred wf, assert wf, rcv? wf, sender wf, Id wf, w-info wf, w-E wf, fair-fifo wf, world wf